\begin{tabbing}
$\forall$${\it es}$:ES, $C$:Type, $S_{1}$, $S_{2}$, ${\it Ack}_{1}$, ${\it Ack}_{2}$:($C$$\rightarrow$$C$$\rightarrow$E$\rightarrow\mathbb{P}$), ${\it Req}_{1}$, ${\it Req}_{2}$:($C$$\rightarrow$E$\rightarrow\mathbb{P}$).
\\[0ex]switch between fifo+ \=s\=end $S_{1}$($j$,$i$,$e$)\+\+
\\[0ex]request ${\it Req}_{1}$($i$,$e$)
\\[0ex]acknowledge ${\it Ack}_{1}$($j$,$i$,$e$) and
\-\\[0ex]send $S_{2}$($j$,$i$,$e$) request ${\it Req}_{2}$($i$,$e$) acknowledge ${\it Ack}_{2}$($j$,$i$,$e$)
\-\\[0ex]$\in$ $\mathbb{P}$
\end{tabbing}